Nuprl Lemma : vartype-es-state-sub 11,40
es:event_system{i:l}, i:Id, ds1,ds2:fpf(Id; x.Type).
fpf-sub(Id; x.Type; id-deq; ds2; ds1)
 (x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds1; id-deq; x; top)))
 subtype_rel(es-state(es; i); decl-state(ds2)) 
latex

Definitionses-state(es; i), decl-state(ds), fpf-sub(A; a.B(a); eq; f; g), fpf(A; a.B(a)), event_system{i:l}, P  Q, x. t(x), id-deq, fpf-cap(f; eq; x; z), top, es-vartype(es; i; x), x:A. B(x), t  T, Id
Lemmassubtype-fpf-cap-top, Id wf, subtype rel self, top wf, id-deq wf, fpf-cap wf, es-vartype wf, subtype rel dep function, event system wf, fpf wf, fpf-sub wf

origin